{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}
{-# OPTIONS -fallow-overlapping-instances #-}
-----------------------------------------------------------------------------
-- |
-- Maintainer  :  joost.visser@di.uminho.pt, alcino@di.uminho.pt
-- Stability   :  experimental
-- Portability :  portable
--
-- Type-safe representation of types at the value level, including
-- representation of recursive types as fixpoints of functors.
--
-- See
--
--     Type-safe Two-level Data Transformation
-- 
-- by
--
--     Alcino Cunha, Jose Nuno Oliveira, Joost Visser
--
-----------------------------------------------------------------------------

module Data.Transform.Type where

import Data.Set as Set
import Data.Map as Map
import Control.Monad
import Data.List as List (intersperse, map, filter)
import Data.Maybe 
-----------------------------------------------------------------------------
-- * Representation of Types

-- | A type-safe representation of types.
data Type a where

    -- Without fixpoints
    Int :: Type Int
    Bool :: Type Bool
    Char :: Type Char
    String :: Type String
    One :: Type One
    Maybe  :: Type a -> Type (Maybe a) 
    List :: Type a -> Type [a]
    Set :: Type a -> Type (Set a)
    Map :: Type a -> Type b -> Type (Map a b)
    Either :: Type a -> Type b -> Type (Either a b)
    Prod :: Type a -> Type b -> Type (a,b)
    Func :: Type a -> Type b -> Type (a -> b)
    Tag :: String -> Type a -> Type a

    -- Constraints    
    TInv   :: Type a -> PF (Pred a) -> Type a

    -- Type variables, mainly for debugging
    TVar   :: String -> Type Dynamic

    -- Fixpoints
    Mu :: Dist f => Fctr f -> Type (Mu f)
    
    -- Additional
    PF :: Type a -> Type (PF a)
    Dynamic :: Type Dynamic

-- | A type-safe representation of lifted functors.
data Fctr f where
    Id    :: Fctr Id
    K     :: Type a -> Fctr (K a)
    (:+:) :: Fctr g -> Fctr h -> Fctr (g:+:h)
    (:*:) :: Fctr g -> Fctr h -> Fctr (g:*:h)
    (:@:) :: Functor g => (forall a . Type a -> Type (g a)) -> Fctr h -> Fctr (g:@:h)

instance Show (Type a) where
    show Int = "Int"
    show Bool = "Bool"
    show Char = "Char"
    show String = "String"
    show One = "One"
    show (Maybe x) = "(Maybe " ++ (show x) ++ ")"
    show (List x) = "(List "++(show x)++")"
    show (Set x) = "(Set "++(show x)++")"
    show (Map x y) = "(Map "++(show x)++" "++(show y)++")"
    show (Either x y) = "(Either "++(show x)++" "++(show y)++")"
    show (Prod x y) = "(Prod "++(show x)++" "++(show y)++")"
    show (Func x y) = "("++show x++" -> "++show y++")"
    show (Tag n t) = "(Tag "++(show n)++" "++(show t)++")"
    
    show (TInv t r) = "(TInv "++ (show t)++" "++(gshow (PF (Func t Bool)) r)++")"
    show (TVar s)   = "(TVar "++ (show s)++" "++")"

    show (PF a) = "(PF "++show a++")"
    show (Dynamic) = "Dynamic"
    show (Mu f) = "(Mu "++show f++")"

        
instance Show (Fctr f) where
  show Id = "Id"
  show (K t) = "(K "++show t++")"
  show (f:*:g) = "("++show f++":*:"++show g++")"
  show (f:+:g) = "("++show f++":+:"++show g++")"
  show (f:@:g) = "(<?>:@:"++show g++")"
  

----------------------------------------
-- ** Showing types that represent databases

showDB :: [String] -> Type a -> String
showDB ns t = showUses ns t ++ "\n  where\n" ++ showDefs ns t

showDefs :: [String] -> Type a -> String
showDefs [] t                        
  = showDefs [ "t"++show n | n<-[0..] ] t
showDefs (n:ns) (Prod a b)            
  = showDefs ns a ++"\n"++ showDefs ns b
showDefs (n:ns) (TInv (Prod a b) p)   
  = showDefs ns a ++"\n"++ showDefs ns b
showDefs (n:ns) t            
  = "    "++n ++ " = " ++ show t

showUses :: [String] -> Type a -> String
showUses [] t                        
  = showUses [ "t"++show n | n<-[0..] ] t
showUses (n:ns) (Prod a b)            
  = showUses ns a ++" x "++ showUses ns b
showUses (n:ns) (TInv (Prod a b) p)   
  = "("++showUses ns a ++" x "++ showUses ns b++")_"++gshow (PF (Func (Prod a b) Bool)) p
showUses (n:ns) t            
  = n

 
----------------------------------------
-- ** Type One

-- data One
type One = ()

_L :: One
_L = error "Attempt to evaluate _L"

-- instance Show One where
--     show _ = "_L"

----------------------------------------
-- ** Type Dynamic

-- | Dynamic types
data Dynamic where
    Dyn :: Type a -> a -> Dynamic

-- | Apply a generic function to a dynamically typed value.
applyDyn :: (forall a . Type a -> a -> b) -> Dynamic -> b
applyDyn f (Dyn ta a) = f ta a

-- | Turn a function on dynamics into a generic function.
dynApply :: (Dynamic -> b) -> Type a -> a -> b
dynApply f ta a = f (Dyn ta a)

instance Show Dynamic where
    show (Dyn a x) = "Dyn "++(gshow a x)
    
----------------------------------------
-- ** Dynamic types

data DynType where
  DynType :: Type a -> DynType
  
instance Eq DynType where
  DynType a == DynType b = maybe False (const True) (teq a b)
  
instance Show DynType where
  show (DynType a) = "DynType "++show a

----------------------------------------
-- ** Type Pred

-- | Predicates
type Pred a = a -> Bool

-----------------------------------------------------------------------------
-- * Deriving type representations from types.

-- | Typeable class of types for which we can derive representations.
class Typeable a where
    typeof :: Type a

instance Typeable Int where
    typeof = Int

instance Typeable () where
    typeof = One

instance Typeable Bool where
    typeof = Bool

instance Typeable Char where
    typeof = Char

instance (Typeable a, Typeable b) => Typeable (a,b) where
    typeof = Prod typeof typeof

instance (Typeable a, Typeable b) => Typeable (Either a b) where
    typeof = Either typeof typeof

instance (Typeable a, Typeable b) => Typeable (Map a b) where
    typeof = Map typeof typeof

instance (Typeable a, Typeable b) => Typeable (a -> b) where
    typeof = Func typeof typeof

instance Typeable a => Typeable (PF a) where
    typeof = PF typeof

instance Typeable Dynamic where
    typeof = Dynamic

instance Typeable String where
    typeof = String
    
instance Typeable a => Typeable (Maybe a) where
    typeof = Maybe typeof

instance Typeable a => Typeable [a] where
    typeof = List typeof

instance Typeable a => Typeable (Set a) where
    typeof = Set typeof
----------------------------------------------------------------------------
-- * Type-indexed functions

----------------------------------------
-- ** Some generic functions

-- | Explicitly contrain a value to a particular type.
constrain :: Type a -> a -> a
constrain _ a = a

-- | Explicitly coerce a value of a given type to another given type.
coerce :: MonadPlus m => Type a -> Type b -> a -> m b
coerce a b x = do Eq <- teq a b
                  return x

----------------------------------------
-- ** Equality of types

-- | Data type to express type-equality.    
data Equal a b where
    Eq :: Equal a a
    
-- | Test equality of types.
--   If the types are equal, a witness 'Eq' of the equality is returned.
teq :: MonadPlus m => Type a -> Type b -> m (Equal a b)
teq Dynamic Dynamic = return Eq
teq Int Int = return Eq
teq Bool Bool = return Eq
teq Char Char = return Eq
teq One One = return Eq
teq String String = return Eq
teq (Maybe a) (Maybe b) =
    do Eq <- teq a b
       return Eq
teq (List a) (List b) = 
    do Eq <- teq a b
       return Eq
teq (Set a) (Set b) = 
    do Eq <- teq a b
       return Eq
teq (Map a b) (Map c d) =
    do Eq <- teq a c
       Eq <- teq b d
       return Eq
teq (Prod a b) (Prod c d) =
    do Eq <- teq a c
       Eq <- teq b d
       return Eq
teq (Either a b) (Either c d) =
    do Eq <- teq a c
       Eq <- teq b d
       return Eq
teq (Func a b) (Func c d) =
    do Eq <- teq a c
       Eq <- teq b d
       return Eq
teq (PF a) (PF b) = 
    do Eq <- teq a b
       return Eq
teq (Tag _ a) b =
    do Eq <- teq a b
       return Eq
teq a (Tag _ b) =
    do Eq <- teq a b
       return Eq
teq (TInv t p) (TInv t' p') = do
  Eq <- teq t t'
  guard (geq (PF (Func t Bool)) p p')
  return Eq
teq (TVar x) (TVar y) = do
  guard (x==y)
  return Eq
teq (Mu f) (Mu g) = do
  error "Cannot determine equality for Mu's"
teq _ _ = mzero

----------------------------------------
-- ** Equality of values

{-
-- | Generic equality
geq :: Type a -> a -> a -> Bool
geq t x y = xyz t t x y
    where xyz :: Type a -> Type b -> a -> b -> Bool
	  xyz t1 t2 x y = aux (toSpine t1 x) (toSpine t2 y)
	  aux :: Spine a -> Spine b -> Bool
	  aux (_ `As` c1)        (_ `As` c2)         = name c1 == name c2
	  aux (Ap f1 (t1 :| a1)) (Ap f2 (t2 :| a2))  = aux f1 f2 && xyz t1 t2 a1 a2
	  aux _ _ = False
-}

-- | Generic equality
geq :: Type a -> a -> a -> Bool
geq t x y = xyz t t x y
    where xyz :: Type a -> Type b -> a -> b -> Bool
	  xyz t1 t2 x y = aux (toSpine t1 x) (toSpine t2 y)
	  aux :: Spine a -> Spine b -> Bool
	  aux (_ `As` c1)        (_ `As` c2)         = name c1 == name c2
	  aux (Ap f1 (t1 :| a1)) (Ap f2 (t2 :| a2))  = aux f1 f2 && xyz t1 t2 a1 a2
	  aux _ _ = False
-- geq t x y = gcompare t x y == EQ
	  
instance Typeable a => Eq (PF a) where
  x == y = geq (PF typeof) x y

-- | Almost generic compare
gcompare :: Type a -> a -> a -> Ordering
gcompare Int x y = compare x y
gcompare Bool x y = compare x y
gcompare Char x y = compare x y
gcompare String x y = compare x y
gcompare One _ _ = EQ
gcompare (List a) x y = aux x y
  where
    aux [] [] = EQ
    aux [] _  = LT
    aux _  [] = GT
    aux (x:xs) (y:ys) 
     = case gcompare a x y of
         LT -> LT
         GT -> GT
         EQ -> aux xs ys
gcompare (Prod a b) (x1,y1) (x2,y2) 
 = let t = gcompare a x1 x2
   in case t of 
     EQ -> gcompare b y1 y2
     otherwise -> t
gcompare (PF _) (FUN f _) (FUN g _) = compare f g 
gcompare (PF _) ID ID = EQ
gcompare t@(PF (Func a c)) (COMP b f g) (COMP b' f' g')
  = case teq b b' of
      Nothing -> error $ "Missing case gcompare for "++show t
      Just Eq -> case gcompare (PF (Func a b)) g g' of
        EQ   -> gcompare (PF (Func b c)) f f' 
        ord  -> ord 
gcompare t x y = error $  "Missing case gcompare for "++show t++
                          " with "++gshow t x++" and "++gshow t y
-- THE REST IS MISSING !!!



-----------------------------------------------------------------------------
-- * Representation of recursive datatypes.

----------------------------------------
-- ** Standard functors

infixr 5 :+:
infixr 6 :*:
infixr 9 :@:

newtype Id a        = Ident {unIdent :: a}       deriving Eq
newtype K b a       = Const {unConst :: b}       deriving Eq
data (g :+: h) a    = Inl (g a) | Inr (h a)      deriving Eq
data (g :*: h) a    = Pair (g a) (h a)           deriving Eq
newtype (g :@: h) a = Comp {unComp :: g (h a)}   deriving Eq

instance Functor Id where
    fmap f = Ident . f . unIdent

instance Functor (K a) where
    fmap f = Const . id . unConst

instance (Functor f, Functor g) => Functor (f :+: g) where
    fmap f (Inl x) = Inl (fmap f x)
    fmap f (Inr x) = Inr (fmap f x)

instance (Functor f, Functor g) => Functor (f :*: g) where
    fmap f (Pair x y) = Pair (fmap f x) (fmap f y)

instance (Functor g, Functor h) => Functor (g :@: h)
    where fmap f = Comp . fmap (fmap f) . unComp

----------------------------------------
-- ** Fixpoints and recursion patterns

-- | Explicit fixpoint operator
newtype Mu f = In {out :: f (Mu f)}

-- This instance requires -fallow-undecidable-instances.
instance Eq (f (Mu f)) => Eq (Mu f) where
  (In fmf) == (In gmg) = fmf==gmg

-- | Catamorphism or fold
cata :: Functor f => (f a -> a) -> Mu f -> a
cata g = g . fmap (cata g) . out

-- | Anamorphism or unfold
ana :: Functor f => (a -> f a) -> a -> Mu f
ana g = In . fmap (ana g) . g

-- | Natural transformation
nu :: Functor g => (forall a. f a -> g a) -> Mu f -> Mu g
nu t = In . fmap (nu t) . t . out

-- |
nu' :: Functor f => (forall a. f a -> g a) -> Mu f -> Mu g
nu' t = In . t . fmap (nu' t) . out

----------------------------------------
-- ** Functors and monads

-- | Class of functors that distribute over monads.
class Functor f => Dist f where
    dist :: Monad m => f (m a) -> m (f a)

instance Dist Id where
    dist (Ident x) = do y <- x
			return (Ident y)

instance Dist (K a) where
    dist (Const x) = return (Const x)

instance (Dist f, Dist g) => Dist (f :+: g) where
    dist (Inl x) = do y <- dist x
		      return (Inl y)
    dist (Inr x) = do y <- dist x
		      return (Inr y)

instance (Dist f, Dist g) => Dist (f :*: g) where
    dist (Pair l r) = do x <- dist l
			 y <- dist r
			 return (Pair x y)

instance (Dist g, Dist h) => Dist (g :@: h) where
    dist (Comp x) = do y <- return $ fmap dist x
		       z <- dist y
		       return (Comp z)

instance Dist [] where
    dist = sequence


-- | Monadic catamorphism.
mcata :: (Monad m, Dist f) => (f a -> m a) -> Mu f -> m a
mcata g = cata (\x -> dist x >>= g)

-----------------------------------------------------------------------------
-- * Type-safe representation of point-free functions.

-- | GADT to represent point-free functions.
data PF a where
    HOLE :: PF a
    FUN :: String -> (a -> b) -> PF (a -> b)
    BANG :: PF (a -> One)
    PNT :: a -> PF (One -> a)
    ID :: PF (a -> a)
    COMP :: Type b -> PF (b -> c) -> PF (a -> b) -> PF (a -> c)

    CONV :: PF (a -> b) -> PF (b -> a)
    ZIP :: PF (([a], [b]) -> [(Maybe a, Maybe b)])
    UNZIP :: PF ([(Maybe a, Maybe b)] -> ([a], [b]))
    FROMJUST :: PF (Maybe a -> a)

    FST :: PF ((a,b) -> a)
    SND :: PF ((a,b) -> b)
    SPLIT :: PF (a -> b) -> PF (a -> c) -> PF (a -> (b,c))
    PROD :: PF (a -> b) -> PF (c -> d) -> PF ((a,c) -> (b,d))
    SWAP :: PF ((a, b) -> (b, a))
    
    INL :: PF (a -> Either a b)
    INR :: PF (b -> Either a b)
    EITHER :: PF (a -> c) -> PF (b -> c) -> PF (Either a b -> c)
    SUM :: PF (a -> b) -> PF (c -> d) -> PF (Either a c -> Either b d)
    
    AP :: PF ((a -> b, a) -> b)
    CURRY :: PF ((a,b) -> c) -> PF (a -> (b -> c))
    EXP :: PF (a -> b) -> PF ((c -> a) -> (c -> b))
    
    NIL :: PF (One -> [a])
    CONS :: PF ((a,[a]) -> [a])
    LIST :: PF (a -> b) -> PF ([a] -> [b])
    
    LIST2MAP :: PF ([a] -> Map Int a)
    EMPTY :: PF (One -> Map a b)
    INSERT :: PF (((a,b),Map a b) -> Map a b)
    MAP :: PF (b -> c) -> PF (Map a b -> Map a c)
    MAPKEYS :: PF (a -> b) -> PF (Map a c -> Map b c)
    ELEMS :: PF (Map a b -> [b])
    LJOIN :: PF ((Map a b, a -> c) -> Map a (b,c))
    DOM         :: PF (Map a b -> Set a)
    RNG         :: PF (Map a b -> Set b)
    MapJoin1    :: PF ((Map a One, Map (a,b) c) -> (Map a (Map b c)))
    MapUnJoin1  :: PF ((Map a (Map b c)) -> (Map a One, Map (a,b) c))
    MapJoin2    :: PF ((Map a b, Map (a,c) d) -> Map a (b, Map c d))
    MapUnJoin2  :: PF (Map a (b, Map c d) -> (Map a b, Map (a,c) d))

    RCoUnPeither :: PF ((Map a c, Map b c) -> Map (Either a b) c)
    RCoUnMapsum1 :: PF ((Map a One, (Map a b, Map a c)) -> Map a (Either b c))
    RCoUnMapsum2 :: PF ((Map a b, (Map a c, Map a d)) -> Map a (b, Either c d))
    
    SET         :: PF (a -> b) -> PF (Set a -> Set b)
    SETFUSE     :: PF (Set (Set a) -> Set a)
    
    MAYBE :: PF (a -> b) -> PF (Maybe a -> Maybe b)
    
    -- To represent contraints
    SetInc      :: Type b -> PF (a -> Set b) -> PF (a -> Set b) -> PF (Pred a)
    AND         :: PF (Pred a) -> PF (Pred a) -> PF (Pred a)
    
    -- meta stuff
    AddProperty :: c -> PF (Map a b -> Map a (b, c)) 
    RemoveProperty :: PF (Map a (b, c) -> Map a b)

    -- RDB 2 SS
    -- list composition
    CompList   :: PF ([(a, b)] -> [(b, b)])
    -- list id
    ListId     :: PF ([(a, b)] -> [(b, b)])
    -- losing the repeated...
    LIST2SET    :: PF ([a] -> Set a)

    -- new RDB 2 SS rules
    -- rule 1 of the paper
    Table2sstable :: PF (Map a b -> [(a, b)])
    Sstable2table :: PF ([(a, b)] -> Map a b)
          
   -- rule 2 of the paper
    Tables2table    :: PF ((Map a b, Map a d) -> Map a (d, Maybe b))
    Table2tables    :: PF (Map a (d, Maybe b) -> (Map a b, Map a d))


    
-- ** Shorthands

infixr 6 .*.
infixr 7 .=<.

f .*. g    = COMP typeof f g
p .=<. q   = SetInc typeof p q

-- dom r = Rdom typeof r
-- rng r = Rrng typeof r
-- inv r = Rinv r



instance (Typeable a, Typeable b) => Show (PF (a->b)) where
  show f = gshow typeof f
{-
  show (FUN s _) = s
  show BANG = "bang"
  show (PNT a ) = "(PNT"++"_)"       
  show ID  = "id"
  show (COMP t f g) = "("++show f++" . "++show g++")"
  show FST  = "fst"
  show SND  = "snd"
  show (SPLIT f g) = "("++show f++" /\\ "++show g++")"
  show (PROD f g) = "("++show f++" >< "++show g++")"
  show INL  = "inl"
  show INR  = "inr"
  show (EITHER f g) = "("++show f++" \\/ "++show g++")"
  show (SUM f g) = "("++show f++" -|- "++show g++")"
  show AP = "ap"
  show (CURRY f) = "(curry"++show f++")"
  show (EXP f) = "(exp"++show f++")"
  show NIL   = "nil"
  show CONS  = "cons"
  show (LIST f) = "(List.map "++show f++")"
  show (LIST2MAP) = "list2map"
  show EMPTY = "empty"
  show INSERT = "insert"
  show (MAP f) = "(Map.map "++show f++")"
  show (MAPKEYS f) = "(Map.mapKeys "++show f++")"
  show ELEMS = "elems"
  show LJOIN = "ljoin"
  show (SET f) = "(Set.map "++show f++")"
-}


-- Evaluation of point-free terms VERY INCOMPLETE!

eval :: PF a -> a
eval (FUN n f) = f
eval BANG = const _L
eval (PNT x) = const x
eval ID = id
eval (COMP _ f g) = eval f . eval g
eval FST = fst
eval SND = snd
eval (SPLIT f g) = \x -> (eval f x, eval g x)
eval (PROD f g) = \(x,y) -> (eval f x, eval g y)
eval INL = Left
eval INR = Right
eval (EITHER f g) = either (eval f) (eval g)
eval (SUM f g) = either (Left . eval f) (Right . eval g)
eval AP = uncurry ($)
eval (CURRY f) = curry (eval f)
eval (EXP f) = (.) (eval f) 
eval NIL = const []
eval CONS = uncurry (:)
eval (LIST f) = Prelude.map (eval f)
eval LIST2MAP = Map.fromDistinctAscList . (zip [0..])
eval EMPTY = const Map.empty
eval INSERT = error "eval INSERT is undefined"
eval (MAP f) = Map.map (eval f)
eval (MAPKEYS f) = Map.mapKeysMonotonic (eval f) -- Wrong!!
eval ELEMS = Map.elems
eval LJOIN = error "eval LJOIN is undefined"
eval (SET f) = Set.mapMonotonic (eval f) -- Wrong!!
eval (MAYBE f) = maybe Nothing (Just . (eval f))
eval DOM = Map.keysSet
eval RNG = Set.fromDistinctAscList . Map.elems -- Wrong!! (fails w/repeated values)
eval MapJoin1 =  \x -> let a = Map.keys  (fst x)
                           b = Prelude.map (snd) (Map.keys (snd x))
                           c = Map.elems (snd x)
                           m1 = zip b c
                           m1'= aux m1
                           m2 = Map.fromDistinctAscList (zip a m1')
                       in Map.map (Map.fromDistinctAscList) m2
eval MapUnJoin1= let (dom,rng) = ((foldr ((++) . Map.keys) []) . (Map.elems),(foldr ((++) . Map.elems) []) . (Map.elems))
                 in \x -> ((Map.map (\y -> () ) x), Map.fromDistinctAscList  (zip (zip (Map.keys x) (dom x)) (rng x)))
eval MapJoin2 = \x -> let a  = Map.keys (fst x)                           
                          b  = Map.elems (fst x)
                          c = Prelude.map (snd) (Map.keys (snd x)) 
                          d = Map.elems (snd x)  
                          m1 = zip c d         
                          m1'= aux m1         
                          m2 = zip a (zip b m1')      
                          m3 = Map.fromDistinctAscList m2         
                      in Map.map (id-><-Map.fromDistinctAscList) m3  
eval MapUnJoin2 = \x -> let l1 = Prelude.map fst  (Map.toList x)                           
                            l2 = Prelude.map fst (Prelude.map snd (Map.toList x))                            
                            a  = Map.fromDistinctAscList (zip l1 l2)  
                            b  = concat (Prelude.map Map.toList (Prelude.map snd (Map.elems x)))  
                        in (a,Map.fromDistinctAscList (zip (zip (Map.keys a) (Prelude.map fst b)) (Prelude.map snd b))) 

eval ZIP = \(l1, l2) -> zip' l1 l2
  where
    zip' (a:as) (b:bs) = (Just a, Just b):(zip' as bs)
    zip' l [] = zip (List.map Just l) (repeat Nothing)
    zip' [] l = zip (repeat Nothing) (List.map Just l)

eval UNZIP = \l -> unzip' l
  where
    unzip' l = let clean = (List.map fromJust) . (List.filter (maybe False (const True)))
               in (clean -><- clean) $ unzip l

--eval (CONV f df) = \b -> let a = Set.map f df

-- meta stuff
eval (AddProperty _) = undefined
eval RemoveProperty = undefined

-- RDB 2 SS
-- rule 1
eval Table2sstable = Map.toList                        
eval Sstable2table = Map.fromDistinctAscList

-- rule 2
eval Tables2table = undefined
eval Table2tables = undefined

-- | this doesn't work... but I don't have equality
eval CompList = \l -> let l1 = List.map (\(a, b) -> (b, a)) l
                      in [(b, b') | (b, a) <- l1, (a, b') <- l]
                      -- in [(b, b') | (b, a) <- l1, (a', b') <- l, a == a']

eval ListId = \l -> [(b, b) | (a, b) <- l]

-- | don't have equality...
eval (SetInc t f1 f2) = \s -> undefined -- Set.isSubsetOf (f1 s) (f2 s)

-- list2set
eval LIST2SET = undefined -- \l -> Set.fromList l




aux [] = [] 
aux ((a,b):t) = [(a,b)]:(aux t) 

infix 5 -><-
infix 4 /\
(f -><- g) (x,y) = (f x,g y)
(/\) f g x = (f x, g x)

-- | Check contraints for values
checkConstraints :: Type t -> t -> Bool
checkConstraints Int _        = True
checkConstraints Bool _       = True
checkConstraints Char _       = True
checkConstraints String _     = True
-- checkConstraints Float _      = True
checkConstraints One _        = True
checkConstraints (Maybe t) y  = maybe True (checkConstraints t) y
checkConstraints (List t) l   = and $ Prelude.map (checkConstraints t) l
checkConstraints (Set t) y
   = and $ Prelude.map (checkConstraints t) (Set.toList y)
checkConstraints (Map t1 t2) m
   = (and $ Prelude.map ((checkConstraints t1) . fst) l) &&
     (and $ Prelude.map ((checkConstraints t2) . snd) l)
     where l = Map.toList m
checkConstraints (Either t1 t2) x
   = either (checkConstraints t1) (checkConstraints t2) x
checkConstraints (Prod t1 t2) (x,y) 
   = (checkConstraints t1 x) && (checkConstraints t2 y)
checkConstraints (TInv t r) x = eval r x && checkConstraints t x
checkConstraints (TVar _) _ = True

-----------------------------------------------------------------------------
-- * Type-indexed functions

-- | Generic show function.
gshow :: Type a -> a -> String
gshow Dynamic (Dyn t x) = gshow t x
-- gshow Int i = show i
-- gshow One _ = "()"
-- gshow Bool x = show x
-- gshow Char x = show x
-- gshow String x = show x
-- gshow (Prod a b) (x,y) = "("++(gshow a x)++","++(gshow b y)++")"
-- gshow (Either a b) (Left y) = "Left ("++(gshow a y)++")"
-- gshow (Either a b) (Right y) = "Right ("++(gshow b y)++")"
-- gshow (List a) l = "["++(concat $ intersperse "," $ fmap (gshow a) l)++"]"
-- gshow (Map a b) m 
--   = "{"++(concat $ intersperse "," $ fmap aux (Map.toList m))++"}"
--   where aux (x,y) = (gshow a x)++":="++(gshow b y)
-- gshow (Set a) s 
--   = "{"++(concat $ intersperse "," $ fmap (gshow a) (Set.elems s))++"}"
-- gshow (Tag n a) x = n++"="++(gshow a x)
{-
gshow (Mu f) (In x) = maybe "Mu <f>" id aux
  where
    aux :: Maybe String
    aux = do
      (View rep fmf) <- applyF f (Mu f)
      return $ gshow fmf $ (to rep) x
-}
gshow t x   =  aux (toSpine t x)
  where
    aux :: Spine a -> String
    aux (Ap (Ap (_ `As` c) (a :| x)) (b :| y)) 
      | fixity c == Infix 
      = "(" ++ gshow a x ++ " " ++ name c ++ " " ++ gshow b y ++ ")"
    aux (_ `As` c)       = name c
    aux (Ap f (t :| a))  =  "(" ++ aux f ++ " " ++ gshow t a ++ ")"



{-
-- | Generic comparison function.
--   Currently defined only for products and integers....
gcompare :: Type a -> a -> a -> Ordering
gcompare Int x y = compare x y
gcompare (Prod a b) (x1,y1) (x2,y2) 
 = let t = gcompare a x1 x2
   in case t of 
     EQ -> gcompare b y1 y2
     otherwise -> t
-}

-----------------------------------------------------------------------------
-- * Spine representation and associated functions

-- SYB reloaded

rmConstraints :: Type a -> Type a
rmConstraints (List a)     = List (rmConstraints a)
rmConstraints (Set a)      = Set (rmConstraints a)
rmConstraints (Map a b)    = Map (rmConstraints a) (rmConstraints b)
rmConstraints (Either a b) = Either (rmConstraints a) (rmConstraints b)
rmConstraints (Prod a b)   = Prod (rmConstraints a) (rmConstraints b)
rmConstraints (Func a b)   = Func (rmConstraints a) (rmConstraints b)
rmConstraints (Tag a b)    = Tag a (rmConstraints b)
rmConstraints (TInv t _)   = rmConstraints t
rmConstraints (Mu f)       = Mu f -- should descend into f as well...
rmConstraints (PF a)       = PF (rmConstraints a)
rmConstraints x            = x

toSpine :: Type a -> a -> Spine a
-- Types
toSpine Dynamic (Dyn t x) = Ap ((Dyn t) `As` dyncon) (t :| x)
toSpine Int n = n `As` (intcon n)
toSpine Bool n = n `As` (intcon n)
toSpine Char n = n `As` (intcon n)
toSpine String n = n `As` (intcon n)
toSpine One x = x `As` bangcon
toSpine (List Int) l = l `As` somelist
toSpine (Either a _) (Left x) = Ap (Left `As` Con{name="Left", fixity=Prefix}) (a :| x)
toSpine (Either _ b) (Right y) = Ap (Right `As` Con{name="Left", fixity=Prefix}) (b :| y)
-- Functions
toSpine (PF _) HOLE = HOLE `As` holecon
toSpine (PF (Func a b)) (FUN n f) = (FUN n f) `As` (varcon n)
toSpine (PF _) BANG = BANG `As` bangcon
toSpine (PF (Func one a)) (PNT x) = Ap (PNT `As` pntcon) (a :| x)
toSpine (PF _) ID = ID `As` idcon
toSpine (PF (Func a c)) (COMP b f g) = Ap (Ap ((COMP b) `As` compcon) (PF (Func b c) :| f)) (PF (Func a b) :| g)
toSpine (PF _) FST = FST `As` fstcon
toSpine (PF _) SND = SND `As` sndcon
-- toSpine (PF (Func a (Prod b c))) (SPLIT f g) = Ap (Ap (SPLIT `As` splitcon) (PF (Func a b) :| f)) (PF (Func a c) :| g)
toSpine (PF t) (SPLIT f g) = Ap (Ap (SPLIT `As` splitcon) (PF (Func a b) :| f)) (PF (Func a c) :| g)
  where  a = domType t
         b = fstType . rngType $ t
         c = sndType . rngType $ t
-- toSpine (PF (Func (Prod a c) (Prod b d))) (PROD f g) = Ap (Ap (PROD `As` prodcon) (PF (Func a b) :| f)) (PF (Func c d) :| g)
toSpine (PF t) (PROD f g) = Ap (Ap (PROD `As` prodcon) (PF (Func a b) :| f)) (PF (Func c d) :| g)
  where  a = fstType . domType $ t
         b = fstType . rngType $ t
         c = sndType . domType $ t
         d = sndType . rngType $ t
toSpine (PF _) INL = INL `As` inlcon
toSpine (PF _) INR = INR `As` inrcon
toSpine (PF (Func (Either a b) c)) (EITHER f g) = Ap (Ap (EITHER `As` eithercon) (PF (Func a c) :| f)) (PF (Func b c) :| g)
toSpine (PF (Func (Either a c) (Either b d))) (SUM f g) = Ap (Ap (SUM `As` sumcon) (PF (Func a b) :| f)) (PF (Func c d) :| g)
toSpine (PF _) AP = AP `As` apcon
toSpine (PF (Func a (Func b c))) (CURRY f) = Ap (CURRY `As` currycon) (PF (Func (Prod a b) c) :| f) 
toSpine (PF (Func (Func _ a) (Func _ b))) (EXP f) = Ap (EXP `As` expcon) (PF (Func a b) :| f) 
toSpine (PF _) NIL = NIL `As` nilcon 
toSpine (PF _) CONS = CONS `As` conscon 
-- toSpine (PF (Func (List a) (List b))) (LIST f) = Ap (LIST `As` listcon) (PF (Func a b) :| f)
--toSpine (PF (List (Prod a b)) (Map a' b')) _ = LIST `As` listcon --Ap (LIST `As` listcon) (PF (Func a b) :| f)
toSpine (PF t) (LIST f) = Ap (LIST `As` listcon) (PF (Func a b) :| f)
  where  a = eltType . domType $ t
         b = eltType . rngType $ t
toSpine (PF _) LIST2MAP = LIST2MAP `As` list2mapcon
toSpine (PF _) LIST2SET = LIST2SET `As` list2setcon
toSpine (PF _) EMPTY = EMPTY `As` emptycon 
toSpine (PF _) INSERT = INSERT `As` insertcon 
-- toSpine (PF (Func (Map a b) (Map _ c))) (MAP f) = Ap (MAP `As` mapcon) (PF (Func b c) :| f)
toSpine (PF t) (MAP f) = Ap (MAP `As` mapcon) (PF (Func b c) :| f)
  where  b = rngType . domType $ t
         c = rngType . rngType $ t
-- toSpine (PF (Func (Map a c) (Map b _))) (MAPKEYS f) = Ap (MAPKEYS `As` (Con "mapkeys" Prefix)) (PF (Func a b):| f)
toSpine (PF t) (MAPKEYS f) = Ap (MAPKEYS `As` (Con "mapkeys" Prefix)) (PF (Func a b):| f)
  where  a = domType . domType $ t
         b = domType . rngType $ t
toSpine (PF _) ELEMS = ELEMS `As` elemscon
toSpine (PF _) LJOIN = LJOIN `As` ljoincon
toSpine (PF _) DOM = DOM `As` (Con "dom" Prefix)
toSpine (PF _) RNG = RNG `As` (Con "rng" Prefix)
toSpine (PF _) MapJoin2 = MapJoin2 `As` (Con "MapJoin2" Prefix)
toSpine (PF _) MapUnJoin2 = MapUnJoin2 `As` (Con "MapUnJoin2" Prefix)
-- toSpine (PF (Func (Set a) (Set b))) (SET f) = Ap (SET `As` (Con "set" Prefix)) (PF (Func a b):| f)
toSpine (PF t) (SET f) = Ap (SET `As` (Con "set" Prefix)) (PF (Func a b):| f)
  where  a = eltType . domType $ t
         b = eltType . rngType $ t 
toSpine (PF _) SETFUSE = SETFUSE `As` (Con "setfuse" Prefix)
-- toSpine (PF (Func a Bool)) (SetInc b x y) = Ap (Ap (SetInc b `As` (Con "=<" Infix)) (PF (Func a (Set b)):| x)) (PF (Func a (Set b)) :| y)
toSpine (PF t) (SetInc b x y) = Ap (Ap (SetInc b `As` (Con "=<" Infix)) (PF (Func a (Set b)):| x)) (PF (Func a (Set b)) :| y)
  where  a = domType t
toSpine (PF t) (AND p q) = Ap (Ap (AND `As` (Con "&&" Infix)) (PF t :| p)) (PF t :| q) 
-- Dropping invariants, gives non-termination!
--toSpine (PF (Func (TInv t _) t')) f = trace "." $ toSpine (PF (Func t t')) f
toSpine (PF (Func (TInv t _) t')) f = toSpine (PF (Func t t')) f
-- toSpine (PF (Func t (TInv t' _))) f = trace ":" $ toSpine (PF (Func t t')) f

 -- where  a = domType t

-- RDB 2 SS
toSpine (PF _) CompList = CompList `As` (Con "compList" Infix)
toSpine (PF _) ListId = ListId `As` (Con "listId" Prefix)

toSpine (PF _) Table2sstable = Table2sstable `As` (Con {name = "table2sstable", fixity = Prefix})
toSpine (PF _) Sstable2table = Sstable2table `As` (Con {name = "sstable2table", fixity = Prefix})

toSpine (PF _) Tables2table = Tables2table `As` (Con {name = "tables2table", fixity = Prefix})
toSpine (PF _) Table2tables = Table2tables `As` (Con {name = "table2tables", fixity = Prefix})

-- meta stuff
toSpine (PF _) (AddProperty x) = (AddProperty x) `As` addProperty 
toSpine (PF _) RemoveProperty = RemoveProperty `As` removeProperty

toSpine t a = error $ "toSpine missing case for "  ++ (show t)


domType :: Type (f a b) -> Type a
domType (Func a b)  = a
domType (Map  a b)  = a
domType (Prod a b)  = a
domType (TInv t _)  = domType t

rngType :: Type (f a b) -> Type b
rngType (Func a b)  = b
rngType (Map  a b)  = b
rngType (Prod a b)  = b
rngType (TInv t _)  = rngType t

fstType = domType
sndType = rngType

eltType :: Type (f a) -> Type a
eltType (Set a)     = a
eltType (List a)    = a
eltType (TInv t _)  = eltType t
--eltType (Maybe a)   = a

data Typed a = Type a :| a

data Spine a where
    As :: a -> Con -> Spine a
    Ap :: Spine (a -> b) -> Typed a -> Spine b

data Fixity = Prefix | Infix deriving Eq

data Con = Con {name :: String, fixity :: Fixity}

fromSpine :: Spine a -> a
fromSpine (c `As` _) = c
fromSpine (Ap f (_ :| a)) = (fromSpine f) a

dyncon = Con {name = "Dyn", fixity = Prefix}
intcon n = Con {name = show n, fixity = Prefix}
onecon = Con {name = "_L", fixity = Prefix}
holecon = Con {name = "_", fixity = Prefix}
bangcon = Con {name = "bang", fixity = Prefix}
idcon = Con {name = "id", fixity = Prefix}
compcon = Con {name = ".", fixity = Infix}
fstcon = Con {name = "fst", fixity = Prefix}
sndcon = Con {name = "snd", fixity = Prefix}
splitcon = Con {name = "/\\", fixity = Infix}
prodcon = Con {name = "><", fixity = Infix}
inlcon = Con {name = "inl", fixity = Prefix}
inrcon = Con {name = "inr", fixity = Prefix}
eithercon = Con {name = "\\/", fixity = Infix}
sumcon = Con {name = "-|-", fixity = Infix}
apcon = Con {name = "ap", fixity = Prefix}
currycon = Con {name = "curry", fixity = Prefix}
expcon = Con {name = "exp", fixity = Prefix}
varcon n = Con {name = n, fixity = Prefix}
pntcon = Con{name = "pnt", fixity = Prefix}

nilcon = Con{name="nil", fixity=Prefix}
conscon = Con{name="cons", fixity=Prefix}
listelimcon = Con{name="listelim", fixity=Prefix}
listfoldcon = Con{name="listfold", fixity=Prefix}
listcon = Con{name="list", fixity=Prefix}
list2mapcon = Con{name="list2map", fixity=Prefix}
list2setcon = Con{name="list2set", fixity=Prefix}

emptycon = Con{name="empty", fixity=Prefix}
insertcon = Con{name="insert", fixity=Prefix}
mapfoldcon = Con{name="mapfold", fixity=Prefix}
mapfoldccon = Con{name="mapfoldc", fixity=Prefix}
elemscon = Con{name="elems", fixity=Prefix}
ljoincon = Con{name="ljoin", fixity=Prefix}
mapcon = Con{name="map", fixity=Prefix}

somelist = Con{name="[...]",fixity=Prefix}

-- meta stuff
addProperty = Con {name = "addProperty", fixity = Prefix}
removeProperty = Con {name = "removeProperty", fixity = Prefix}

-----------------------------------------------------------------------------
